perm filename SECOND.DOC[1,JRA]1 blob
sn#022407 filedate 1973-02-02 generic text, type T, neo UTF8
Preliminary User Manual February 2, 1973
Preliminary User's Manual for the Theorem Prover
The current program is a resolution- and paramodulation-based theorem
prover with extensive facilities for on-line control. Perhaps the
easiest introduction is to follow the development of a few examples.
Example 1.
Consider the following set of statements:
(1) (∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}
(2) (∀y∃x){P(x,y)}
We might interpret these statements as claiming
"For all x and y, if x is the parent of y and y is the parent
of z, then x is the grandparent of z,"
and
"Everyone has a parent."
Given these statements as hypotheses we might wish to know if there
were individuals, x and y such that x is the grandparent of y. We
could pose that question as the statement:
(3) (∃x∃y){G(x,y)}
It is clear that (3) does indeed follow from (1) and (2). How do we
formulate the problem for the theorem prover?
Here is one axiomatization:
∀(x1 x2)(P(x1 x2) ∧ P(x2 x3) ⊃ G(x1 x3)); ;
∀(x2)∃(x1)P(x1 x2); ;
∃(x1 x2)G(x1 x2); ;
That is, variables are represented as "subscripted x's ", and each
statement is terminated by a semicolon. The input statements are
also expected to be partitioned into three sets: the axioms, the
hypotheses, and the theorem to be proved. Each set of statements is
also terminated by a semicolon.
Preliminary User Manual February 2, 1973
Example 2.
In an investigation of axiomatizations of elementary group theory the
following statements arose:
(1) x*x = y*y
(2) x*(y*y) = x
(3) x*(y*z) = z*(y*x)
(4) x*(x*y) = y
(5) (x*z)*(y*z) = x*y
Question: Does (5) follow from (1)-(4)?
The answer is "yes" but it is not immediately obvious. It is more
difficult to establish than Example 1. Notice that this Example is a
pure equality formulation, requiring only replacements of terms by
other terms. This example could be presented to the prover as:
E(F(X1 X1) F(X2 X2));
E(F(X1 F(X2 X2)) X1);
E(F(X1 F(X2 X3)) F(X3 F(X2 X1)));
E(F(X1 F(X1 X2)) X2); ;
;
E(F(F(X1 X3) F(X2 X3)) F(X1 X2)); ;
Before presenting a more complicated example, we shall describe how
to use the prover on these first Examples.
Preliminary User Manual February 2, 1973
Once the input file has been prepared you are ready to used the
theorem prover. The command: RUN PROVER [P,JRA] , will select the
current version of the program. The appearence of an asterisk (*)
signifies that the program is ready. If you wish the program to make
an initial selection of strategies for your problem then type:
(PROVE DSK: filename). The exact strategies which are chosen are
described in a later section. The program will however ask whether
the equality replacement rule is to be applied.
(IS THERE AN EQUALITY PREDICATE (Y/ N))
If you do respond, "Y", then the program wants to know which
predicate letter is to be interpreted as equality.
(WHAT IS IT)
if you would rather select you own strategies then type: (TRY DSK:
filename). You will then be asked to respond to a series of
questions concerning selection of editing and choice strategies.
THE-FOLLOWING-CHOICE-STRATEGIES-ARE-AVAILABLE: <list of
available strategies> ;see pg.[ ] for the current strategies
and their meaning. PICK-SOME
Unless no choice strategies are desired (signified by typing NONE)
the prover wiil ask if more are desired. If no more are desired, type
N or NO. The strategy used in the proof attempt will be the
conjunction of the selected strategies.
In either mode of operation, TRY or PROVE, the program begins
Preliminary User Manual February 2, 1973
operation as soon as it has sufficient information from the user. If
the set of statements consisting of the axioms, hypotheses and the
negation of the theorem is found to be inconsistent, then the
sequence of deductions which exhibits that inconsistency is displayed
on the console. This refutation and the set of strategies which were
employed are also saved on a disk file . The name of the file is
created from the name of the input file,differing only in having the
extension, PRF. Thus, for example, (PROVE DSK: FOO) and (PROVE DSK:
(FOO.A)) would create an output file named FOO.PRF. If the input
initially comes for the console using (PROVE) or (TRY), then the
output file is given the name, PRF.PRF. It is also possible that
the prover terminate without finding a refutation. This could occur
either because the selected strategies do not form a complete set or
because the initial set is not inconsistent. In either case the
program types NO-PROOF-FOUND and enters the clause editor to wait
for commands from the user.
Preliminary User Manual February 2, 1973
Now let's try running the first example. Assume that a disk file,
EX1, has been prepared containing the axiomatization. What follows is
a running commentary on what should occur. Material preceeded by | is
commentary; statements typed by the user are preceeded by *.
*RUN PROVER [P,JRA] |retrieve the current prover.
*(PROVE DSK: EX1) |Request that the program pick the
|strategies while running EX1.
TYPE-AXIOMS: |The program is accepting the axioms.
TYPE-HYPOTHESES:
TYPE-THEOREM:
HERE-ARE-THE-CLAUSES: |What follows are the translations
|of the input into clause-form, with
G(X1,X2) ¬P(X3,X2) ¬P(X1 X3) |the redundant statements removed.
P(HYP65(X1),X1) |HYP65 is a generated Skolem function
¬G(X1,X2) |The translation of the negation of
(IS THERE AN EQUALITY PREDICATE (Y / N)?) |the theorem.
*N |There is no equality predicate.
4 ¬P(X1,X2) -P(X3 X1) |A deduction which has been added to
|the list of clauses.
COUNT = 1 |There was only one resolvent formed
LEVEL = 1 |on level one.
ELAPSED-TIME = 333 |The execution time in milliseconds.
5 ¬P(X1 X2)
COUNT = 3
LEVEL = 2 |Three resolvents have been formed by
ELAPSED-TIME = 500 |the end of level 2. (Two have been
|retained.)
NIL 1 4 |A contradiction. These next six
1 -P(X1 X2) 3 4 |lines are the refutation. I.e.:
3 ¬P(X1,X2) ¬P(X3 X1) 5 6 | 6 5
4 P(HYP65(X1), X1) HYP 1 | \ /
5 G(X1,X2) ¬P(X3,X2) ¬P(X1 X3) AX 1| 3 4
6 ¬G(X1,X2) THM 1 | \ /
| 1 4
| \ /
| NIL
Preliminary User Manual February 2, 1973
Notes:
1. Each clause -- deduction or translation of input -- is a
disjunction of the literals which appear. For example,
¬P(X1,X2) ¬P(X3,X1), represents ¬P(X1,X2) ∨ ¬P(X3,X1).
2. The partition of the input into the three sets is
reflected in the description of the refutation tree. That is,
P(HYP65(X1),X1) resulted from the translation of one of the
hypotheses; ¬G(X1,X2) came from the negation of the theorem.
3. A copy of the refutation tree, relevant statistics, and a
description of the actual strategies used, now appears on a
file named EX1.PRF.
Preliminary User Manual February 2, 1973
Now let's run the second example. Assume that the axiomatization is
on a file named EX2.
*RUN PROVER [P,JRA]
*(PROVE DSK: EX2) |Again, let the program
|pick the strategies.
TYPE-AXIOMS
TYPE-HYPOTHESES
TYPE-THEOREM
HERE-ARE-THE-CLAUSES:
E(F(X1,X1),F(X2,X2))
E(F(X1,F(X2,X2)),X1)
E(F(X1,F(X2,X3)),F(X3,F(X2,X1)))
E(F(X1,F(X1,X2)),X1)
¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67))
|Again, THMn's are generated
|Skolem constants.
(IS THERE AN EQUALITY PREDICATE (Y/N)?)
*Y |This time there is.
(WHAT IS IT ?)
*E |E is obviously it.
NIL 1 2 |An immediate contradiction
1 E(X1,X1) |We know E is reflexive
2 ¬E(F(THM66,THM67),F(THM66,THM67)) 3 4 |moderate mystery.
3 E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
4 ¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67)) THM 1
Notes:
1. The `refutation' is a bit mysterious. A more sympathetic proof
recovery mechanism is contemplated, but perhaps some of the current
mystery can be dispelled.
A `natural' proof might be:
1. (x*z)*(y*z) = z*(y*(x*z)) replacement using (3)
2. z*(y*(x*z)) = z*(z*(x*y)) replacement using (3)
3. z*(z*(x*y)) = x*y replacement using (4)
The above proof is indeed a translation of the machine proof.
Besides replacement, the prover also has a special rule of
simplification. Whenever an equality formulation is presented to the
prover, a list ,SL,is made consisting of all the equalities which
occur in the input. In the current example, SL would consist of
Preliminary User Manual February 2, 1973
everything but the negation of the theorem. Let t1 = t2 be a member
of SL. Whenever a deduction is formed (but before it has been added
to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we repalce those
terms with the appropriate instance of t2. It is this simplified
deduction which is presented to the prover.
Thus the refutation really is:
¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67)) THM 1
\
\
\ E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
\ /
\ /
¬E(F(THM68,F(THM67,F(THM66,THM68))),F(THM66,THM67))
\ by replacement
\
\ E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
\ /
\ /
¬E(F(THM68,F(THM68,F(THM66,THM67))),F(THM66,THM67))
\ by simplification
\
\ E(F(X1,F(X1,X2)),X2) AX 4
\ /
\ /
¬E(F(THM66,THM67),F(THM66,THM67))
\ by simplification
\
\ E(X1,X1)
\ /
\ /
NIL
by resolution
Preliminary User Manual February 2, 1973
Most applications of the prover lie in that gray area between a quick
proof and the occurrence of NO-PROOF. That is, an application of the
prover usually generated a large number of deductions before either a
proof is found or no more deductions can be made under the current
strategy settings. It is this area which can be profitably explored
using interactive commands. If the user sees a deduction which
should lead to the desired refutation he is able to guide the
program to the explicit contradiction. If he sees a deduction which
he feels is interesting, he can explore its consequences in the set
of statements. If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.
The next sections give detailed descriptions of the current on-line
commands.
I. GENERAL BOOKEEPING COMMANDS.
CHange CH;
It is frequently desireable to change some of the
strategies while a proof attempt is in progress.
CHange initiates a dialogue with the user describing
what choice and editing strategies are currently
active and asking which are to be changed.
CUrrent CU;
This command simply lists the current strategy
settings.
DSkout DS <filename>;
This command diverts future output to specified disk
file.
EVal EV;
Preliminary User Manual February 2, 1973
This command is mostly a debugging aid and is
included for completeness. The casual users should
not have to resort to its use. EVal enters a READ-
EVAL-PRINT. To return to the editor, type @END.
HAlt HA;
HAlt stops the prover is such a state that if the
current core image is saved, it can be continued. To
resume execution of such a core image, type RUN DSK:
name. When the asterisk appears you are in the on-
line editor. Then type TErminate.
End Of file EO;
EOf is used to terminate the DSkout command.
HElp HE;
This command will type a list of the available
editing commands along with an abbreviated
description of their action.
TErminate TE;
This command is used to terminate the editing process
and return to the prover.
Preliminary User Manual February 2, 1973
II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
Each clause which has been retained by the prover -- axiom,
hypothesis, negation of the theorem or deduction -- is given a numbe,
the first axiom, the number 1., etc.. These numbers are permanently
assigned, even though certain actions of the prover may remove
clauses from consideration by the rules of inference. Clauses which
have been so deleted are displayed as *DE*. When the editor is
entered, a hypothetical pointer is initialized to the first clause.
This first set of commands allow the used to manipulate the set of
clauses using the associated numbers.
FLoat UP FU; or FL UP;
Moves the pointer up through the list of clauses.
The motion is stopped either by striking a key or by
reaching the upper extreme of the list. FLoat UP may
also be apbbreviated as FU.
FLoat DOwn FD; or FL DO;
The counterpart of FLoat UP. FLoat Down may also be
abbreviated as FD.
UP UP n;
UP is to be followed by an integer, N. The effect of
this command is to move the pointer up N clauses from
its current setting. As the pointer is moved, the
interviening clauses are printed. If N = 0, then the
pointer is immediately moved to the beginning of the
clause list. As with the FLoat commands,striking a
key will stop the pointer.
DOwn DO n;
The counterpart of UP. DOwn 0 moves the pointer to
the end of the list.
GO GO n;
Preliminary User Manual February 2, 1973
GO is to be followed by an integer designating a
clauses. The pointer goes immediately to the
designated clause.
Preliminary User Manual February 2, 1973
Though these commands have proved quite useful, experience has
shown that more global manipulation of the clauses is needed.
Therefore we have commands for assigning names to subsets of the
clause list, and commands for manipulating these sets. Just as each
element of the primary list of clauses is assigned a unique positive
integer, so is each element of each named subset. For example to
refer to the second element of the set named FOO, use (FOO 2); to
refer to the second and third elements, use (FOO 2 3). Certain
commands, like REsolve or PAramodualte create new names, like
RES1,RES2, etc. or PAR1, PAR2. These created names are local to that
call on the on-line editor. Names which were initiated by the user
using the SEt command are global.
The following BNF equations will be used in the sequel:
<clauses> := <ind>
:= <clauses><ind>
<ind> := <integer> ;select the designated clause in the clauselist.
:= <name> ;select the designated set of clauses
:= (<name> <soi>);select the designated clauses from <name>
<name>:= <identifier> ;
<soi> := <integer>
:= <soi>,<integer>
CLear CL <name>;
CLear takes a name as argument. This command only
removes the name from the symbol table; it does not
affect the clauses attached to the name.
Preliminary User Manual February 2, 1973
Delete DE <clauses>;
The designated clauses are deleted from the memory of
the prover. Attempts to display such clauses will
print *DE*. Other attempts to use deleted clauses in
editing commands will invoke an error message.
DIsplay DI <clauses>;
This command displays all the elements of <clauses>;_
INsert IN <name> <statements>; IN <name> DSK: <file>;
This command is used to enter new clauses into the
clause editor. The first argument to INsert is a
<name>. What follows is a set of clauses, or a file
designator. If the clauses are typed they must
conform to the standard input format; if a file
designator is given, the specified file must be in
the correct format.
MErge ME <clauses>; <clauses>;
This commnad deletes all clauses from the first set
whichare subsumed by elements of the second set.
SAve SA <clauses>;
Most of the results of the on-line commands:
deductions, insertions, substitutions,etc, are local
to the clause editor. To include any of these
resulting clauses in the memory of the prover use the
Save command.
SEt SE <name> <clauses>;
SEt <name> <clauses>; has the effect of assigning to
<name>, the sequence of clauses selected by the
<clauses>. Within a particular proof attempt, the
names selected by the user are retained.
SUbstitute SU <term1> FOR <term2> IN <clauses>;
This command is used to form substitution instances
of selected clauses. These created instances are
attached to the name, ASSERT. The original clauses
are not affected.
Preliminary User Manual February 2, 1973
The commands listed above give us a reasonably powerful set of
instructions for manipulating the clause list. Clearly, before we can
really begin to guide the prover we must be able to perform the rules
of inference on-line. The next set of commands begins to do this.
III. COMMANDS FOR PERFORMING RULES OF INFERENCE
PAramodulate PA <clauses>; <clauses>;
This command(which cries for abbreviation) is the
counterpart to REsolve. All equality literals of
the form t1=t2, are used in equality replacements in
the following manner: let s be any term, not a
variable, which occurs in some literal in one of the
clauses. If s occurs no deeper than PDEPTH (see the
appendix for PDEPTH) and there is a substitution
unifying s and t1, then the occurrence of t1 is
replaced by the appropriate instantiation of t2.
REsolve RE <clauses>;<clauses>;
This command takes a pair of <clauses> as arguments.
The resolvents of these two sets are formed, a unique
name is generated and the resolvents are assigned to
that new name. The generated names are presently of
the form RESn, for some integer,n.
SImplify SImplify <clauses>; BY <clauses>;
This command is similar to the PA command. Here the
second set of clauses is to be a list of equality
units, again of the form t1=t2. Terms occuring in the
first set of clauses which unify with elements, t1,
are replaced by instances of t2. DDEPTH determines
the depth to which the match is attempted.
Example 3. A simple example of the use of the rules of inference.
Assume that R is the equality predicate and that we have just struck
a key on the console.
*DI 1,2,3; |Display the first three clauses
1 R(D(X1,X2),O) ¬LE(X1,X2)
2 ¬R(D(U,D(A,B)),U)
Preliminary User Manual February 2, 1973
3 LE(O,X1)
*PA 1; 2; |Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1 |PAR1 is a created name.
1 ¬R(U,O) ¬LE(U,D(A,B))
*PA 2; 3; |Try to use the replacement rule
NO-PARAMODULANTS |on clauses 2, and 3.
*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1 |RES1 is another created
|name.
1 R(D(O,X1),O)
*PA RES1; RES1; |Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2 |PAR2 is a new name.
1 R(O,O) |True.
*SA (PAR1 1); |Add this deduction to the memory
|of the prover;
Preliminary User Manual February 2, 1973
IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
Though the commands, REsolve and PAramodulate, are useful for fine
control of the prover, is is often useful to demand larger inference
steps. That is, using some of the existing clauses in memory, with
perhaps some additional assumptions, we wish the prover to attempt to
establish the validity of a first order formula. While this subproof
is under investigation the state of the main proof should be
preserved. The commands in this section are used to initiate and
control such subproofs.
ABort AB ; or AB <clauses>;
This command is used to manually abort a proof
attempt, returning to the previous level. If
<clauses> is present, then the selected clauses are
returned and assigned to a created name.
ASsume AS <statements>; or AS DSK: <file>;
This command introduces the designated statements to
the prover. The statements are assigned to a local
name, ASSUMPTIONS, and will appear as hypotheses
under the name HYPS in the forthcomming subproof.
USing US <clauses>;
The selected clauses in the prover's memory are
designated to be the AXIOMS in the subproof.
PRove PR <statement>; or PR DSK: <file>;
The <statement> is translated and will be attached to
the name LEMMA. The negation of the statement is also
formed and will be used in the subproof. Thus both
the positive and negative tanslates are formed. The
positive translate is maintained for the convenience
of the user since after the lemma has been
established it should be available for further
deductions. Within the subproof the negation of the
<statement> will appear under the local name, THMS.
Preliminary User Manual February 2, 1973
These three commands,--ASs↓C
@α⊂@@ε__↓@αλ_!α∧